$\forall$$E$:Type, ${\it pred?}$:($E$$\rightarrow$(?$E$)), $e$:$E$.
\\[0ex]SWellFounded(($\neg$($\uparrow$first($y$))) c$\wedge$ ($x$ = pred($y$) $\in$ $E$)) $\Rightarrow$ (eventlist(${\it pred?}$; $e$) $\in$ ($E$ List))